k:Knd. (isrcv(k))  (tag(k)  Id) 

latex

Definitions	x:A. B(x), Knd, P  Q, isrcv(k), t  T, tag(k), x. t(x), x(s), prop{i:l}
Lemmas	pi2 wf, IdLnk wf, Id wf, outl wf, assert wf, isl wf